Nuprl Lemma : rng_sum_split 11,40
r:Rng, a, b, c:.
(a  b)
 (b  c)
 (E:({a..c}|r|).
 ((r) a  j < c. E(j)) = (((r) a  j < b. E(j)) +r ((r) b  j < c. E(j)))  |r|) 
latex

Definitionst  T, IMonoid, x:A. B(x), t.2, t.1, , P & Q, Mon, Group{i}, AbGrp, r+gp, *, |g|, (r) i  k < j. E(k)
Lemmasrng wf, abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon itop split

origin